Computer systems, software applications, and the devices and processes built around them are continually growing in power and complexity. Society's reliance on such systems is likewise increasing, making it critical that the systems obey the properties their designers intended. Typically, the more powerful and complex the system, the greater its utility and usefulness. However, as these computer and software implemented systems and processes become more powerful, detecting and correcting flaws within the systems becomes increasingly difficult.
Achieving the desired level of reliability in a complex system thus depends upon being able to analyze the system's design and characteristics early in the design process. In so doing, the consequences of design choices and trade-offs can be explored and tested prior to design implementation, and potentially disastrous flaws can be detected and remedied while their cost of repair is still relatively inexpensive. For example, detecting a flaw in a microprocessor design prior to its mass fabrication is much more desirable and much more economical than correcting the consequences of the flaw after the microprocessor has been deployed in systems throughout the world. Computer engineers and other designers of complex systems use numerous tools to aid in system design and debugging. One of the most powerful of such tools is the "state machine".
A state machine, or state automaton, is an abstract machine consisting of a set of states, a set of input events, a set of output events, and a state transition function. The state transition function takes the current state and an input event and returns a new set of output events and the next state. A state machine is typically depicted as a state transition diagram which consists of circles representing specific states and lines between the states to represent transitions. One or more actions, for example one or more inputs or outputs, are usually associated with each transition.
A state machine may be classified as finite or extended. As its name implies, a finite state machine includes a finite number of states. Finite state machines are typically employed to model complex systems, which in turn, have a finite number of possible states. Each state of the complex system is represented as a state in the finite state machine. If the complex system can be realistically modeled using a state machine, the designer can examine the state machine to determine whether the complex system functions as desired. For example, the designer will examine the states of the state machine and the transitions between the states to determine whether the complex system can achieve all of its "desired states" and determine whether the system successfully avoids all "illegal states". A desired state may represent, for example, correctly calculating a desired result. An illegal state may represent, for example, and error condition which results in system malfunction. This design verification process is referred to as state reachability analysis. The goal of state reachability analysis is to compute the set of all reachable states from an initial state of a complex system, and to use this information to verify the behavior of the complex system.
Hence, a primary goal of state reachability analysis involves proving, in a mathematical sense, that error conditions in the design of a complex system cannot occur. This process is called formal verification. It typically involves using the high-level description language (HDL) design of the complex system to create a state machine model, and analyzing the state machine model to determine therefrom a set of possible states, and analyzing this set of possible states to determine a set of reachable states (e.g., from the initial state). The set of reachable states is then analyzed to determine whether it contains an illegal state (e.g., an error condition). It should be appreciated that this process involves detecting errors in the design of the complex system as opposed to the fabrication of the complex system. For example formal verification cannot detect errors in the fabrication process which result in bad transistors on semiconductor dies. Formal verification does detect errors in the HDL design of microprocessors and other such devices. It is often these design errors which are most difficult to prevent and most difficult to detect prior to widespread deployment of the complex system. For additional details regarding state machines and their theory of operation, please refer to J. H. Conway, "Regular Algebra and Finite Machines", 1971, Eds Chapman & Hall; S. C. Kleene, "Representation of Events in Nerve Nets and Finite Automata", 1956, Automata Studies. Princeton; and Hopcroft & Ullman, 1979, "Introduction to Automata Theory, Languages and Computations", Addison-Wesley.
There is a problem, however, when the size of the complex system becomes quite large. Large complex systems can result in a finite state machine having an unmanageably large number of possible states. For example a modern microprocessor often processes information in data words of up to 64 bits in one cycle. This results in a very large number of inputs and outputs per state, and a very large number of state transitions, and thus an extremely large number of possible states. The large number of inputs and outputs are typically referred to as large "data variables". Large data variables, as often used in a 64-bit microprocessor, leads to an extremely large number of possible states. The large number of possible states makes it hard to determine which of the possible states are actually reachable from the initial state of the microprocessor. This, in turn, makes it very difficult to determine whether the microprocessor can actually reach any illegal states.
Thus, what is desired is a more efficient method and system for state reachability analysis for complex systems having a very large number of possible states. What is desired is an efficient method and system for functional verification of the design of a complex system having a very large number of possible states. What is desired is a system which can efficiently process and analyze a state machine model having an extremely large (or even infinite) number of possible states. The present invention provides a novel solution to the above requirements.